\chapter{Automi Comportamentali}
\label{cap:cap_2}
\section{Linguaggio dei contratti}

La \emph{sintassi} dei contratti utilizza un insieme infinito di \emph{nomi} $\mathcal{N}$ (usiamo $a,b,...$  per indicare un nome) e un insieme disgiunto di \emph{co-nomi} $\overline{\mathcal{N}}$ (usiamo $\co a,\co b,...$ per indicare un co-nome). Utilizziamo il temine \emph{azione} per riferirci, senza distinzioni, a \emph{nomi} e \emph{co-nomi} e $\alpha$ per indicare una generica azione dove l'azione interna \`e indicata con $\tau$.
I \emph{contratti} rappresentano il comportamento del servizio Web, quindi l'attivit\`a che un servizio pu\`o svolgere e delineano \emph{come} e \emph{quando} tali attivit\`a possono essere eseguite. Un'attivit\`a \`e definita dalla seguente grammatica:

\[
\begin{array}{rll}
A ::= &  & \textrm{} \\ 
| & \nullc & \textrm{(fallimento)}\\
| & \winc & \textrm{(successo)}\\
| & \alpha & \textrm{(azione)}\\
| & A+A & \textrm{(scelta esterna)}\\
| & A\oplus A & \textrm{(scelta interna)}\\
| & A;A & \textrm{(composizione sequenziale)}\\
| & A|A & \textrm{(composizione parallela)}\\
| & A^\ast & \textrm{(ripetizione esterna)}\\
| & A^\circledast & \textrm{(ripetizione interna)}  
\end{array}
\]

Assumiamo che $A,B,C...$ siano attivit\`a, con la convenzione che $C$ \`e riservato per il comportamento del cliente e $A,B,...$ per il servizio. L'attivit\`a $\winc$ denota sia il cliente sempre soddisfatto sia il servizio che non offre nulla, al contrario di $\nullc$ che rappresenta il cliente mai soddisfatto; l'attivit\`a $\alpha$ denota il cliente soddisfatto dopo aver effettuato l'azione $\alpha$ e il servizio che offre l'azione $\alpha$; tale azione pu\`o essere di input o di output, corrispondente rispettivamente alle specifiche BPEL di receive e invoke/reply. Le attivit\`a $A+B$ e $A\oplus B$ denotano scelte comportamentali, nel senso che vengono eseguite attivit\`a alternative; in $A+B$ la scelta \`e lasciata alla parte remota, inceve in $A\oplus B$ la scelta \`e fatta localmente da chi espone tale comportamento (servizio o cliente). L'attivit\`a $A;B$ denota comportamenti in sequenza, nel senso che $B$ inizier\`a l'esecuzione solo dopo la fine del comportamento di $A$. In alternativa a comportamenti sequenziali abbiamo comportamenti come $A|B$ che permettono l'esecuzione parallela delle attivit\`a coinvolte nell'operazione. Gli ultimi due costrutti definiscono cicli interni, poich\'e il numero di ripetizioni \`e determinato internamente dal processo che espone tale comportamento o esterni, in quanto la numerosit\`a delle ripetizioni \`e a discrezione della parte remota che usufruisce di tale comportamento.
Prima di vedere la semantica dei nostri costrutti definiamo il \emph{predicato di terminazione con successo}, che utilizzeremo nel sistema di transizioni, descritto dalle seguenti regole:

\begin{displaymath}
\winc\checkmark \qquad
A^\ast\checkmark \qquad
\frac{B\checkmark }{A+B\checkmark} \qquad
\frac{A\checkmark}{A+B\checkmark} \qquad
\frac{A\checkmark\qquad B\checkmark}{A;B\checkmark} \qquad
\frac{A\checkmark\qquad B\checkmark}{A|B\checkmark}
%A^\circledast\checkmark \qquad
%\frac{A\checkmark\qquad B\checkmark}{A\oplus B \quad\checkmark} \qquad
\end{displaymath}

Tale predicato definisce quando l'attivit\`a (di un servizio o di un cliente) \`e in uno stato di successo o meglio in uno stato che pu\`o essere considerato di terminazione. Descriviamo brevemente questi predicati: $\winc$ \`e definito come un comportamento di successo, quindi \`e banalmente intuibile il perch\'e si trovi tra questi predicati; $A+B$ termina con successo se una delle scelte alternative ha terminato con successo; $A;B$ termina con successo se e solo se antrambe le attivit\`a terminano con successo, o meglio se, in sequenza, prima l'attivit\`a $A$, poi $B$ terminano positivamente. L'ultimo predicato $|$ termina con successo se entrambe le attivit\`a coinvolte nel parallelismo hanno terminato con successo. I costrutti: $\nullc, \alpha, \oplus, \circledast$, non hanno predicato di terminazione con successo. Per quanto riguarda i primi due la motivazione \`e banale, nel senso che il primo delinea di fatto un comportamento di fallimento e il secondo prima di giungere in uno stato di terminazione con successo dovr\`a effettuare una mossa (visibile) e quindi per definizione non potr\`a essere finale; invece per gli altri due costrutti la motivazione \`e che l'attivit\`a deve eseguire una scelta interna (azione non visibile) su quale comportamento eseguire e quindi per definizione di finale, non pu\`o essere terminata ($\winc$). Una volta delineati questi predicati procediamo con la definizione di \emph{semantica} dei contratti attraverso un sistema di transizioni che fornisce le seguenti regole per ogni costrutto:

\begin{itemize}
\item $\alpha$ :
	\begin{displaymath}
	\alpha \lred{\alpha} \winc
	\end{displaymath}
	
La regola per $\alpha$ dice che data l'attivit\`a $\alpha$ ed una transizione visibile etichettata $\alpha$, il comportamento che scaturisce sar\`a quello di successo.

\item $A+B$ : 
	\begin{displaymath}
	\frac{A \lred{\tau} A'}{A+B \lred{\tau} A'+B} \qquad
	\frac{B \lred{\tau} B'}{A+B \lred{\tau} A+B'} \qquad
	\frac{A \lred{\alpha} A'}{A+B \lred{\alpha} A'} \qquad
	\frac{B \lred{\alpha} B'}{A+B \lred{\alpha} B'} \qquad
	\end{displaymath}
	
La regola per $+$ dice che il comportamento di $A+B$ pu\`o esibire sia $A$ che $B$ eseguendo una transizione visibile, etichettata $\alpha$, rispettivamente di $A$ e di $B$. Una transizione interna, etichettata $\tau$, di $A$ o di $B$ non impedisce alla parte remota di continuare a scegliere il comportamento alternativo.	
	
\item $A\oplus B$ :
	\begin{displaymath}
	A\oplus B \lred{\tau} A \qquad
	A\oplus B \lred{\tau} B \qquad
	\end{displaymath}
	
La regola per $\oplus$ dice che il comportamento di $A\oplus B$ pu\`o esibire sia $A$ che $B$ eseguendo una transizione interna etichettata $\tau$.

\item $A;B$ : 
	\begin{displaymath}
	\frac{A \lred{\alpha} A'}{A;B \lred{\alpha} A';B} \qquad
	\frac{A\checkmark\qquad B \lred{\alpha} B'}{A;B \lred{\alpha} B'} \qquad
	\end{displaymath}
	
La regola per $;$ dice che il comportamento di $A;B$ esibisce per primo $A$, poi quando $A$ \`e terminato con successo esibisce il comportamento di $B$.  
	
\item $A|B$ :
	\begin{displaymath}
	\frac{A \lred{\alpha} A'}{A|B \lred{\alpha} A'|B} \qquad
	\frac{B \lred{\alpha} B'}{A|B \lred{\alpha} A|B'} \qquad
	\end{displaymath}
	
La regola per $|$ dice che il comportamento di $A|B$ pu\`o esibire sia $A$ che $B$ contemporaneamente, nel senso che le due attivit\`a possono essere eseguite in parallelo.
 
\item $A^\ast$ :
	\begin{displaymath}		
	\frac{A \lred{\alpha} A'}{A^\ast \lred{\alpha} A';A^\ast} \qquad
	\end{displaymath}
	
La regola per $^\ast$ dice che il comportamento di $A^\ast$ esibisce $A;A^\ast$ effettuando una transizione visibile (etichettata $\alpha$) di $A$. Questo costrutto ammette comportamenti ricorsivi, in quando esegue $A^\ast$, che riporta allo scenario iniziale ($A;A^\ast$), in sequenza ad $A$.

\item $A^\circledast$ :	
	\begin{displaymath}	
	A^\circledast \lred{\tau} 1 \qquad
	A^\circledast \lred{\tau} A;A^\circledast \qquad
	\end{displaymath}	
	
La regola per $^\circledast$ dice che il comportamento di $A^\circledast$	pu\`o esibire sia $A;A^\circledast$ sia $\winc$, in corrispondenza di una transizione interna etichettata $\tau$. Quindi la scelta di quale attivit\`a eseguire \`e fatta localmente da chi esibisce tale comportamento. L'attivit\`a derivante $A;A^\circledast$ ammette anch'essa un comportamento ricorsivo, in quando esegue $A^\circledast$, che riporta allo scenario iniziale, in sequenza ad $A$.
\end{itemize}
Passiamo ora a definire i nostri Automi Comportamentali (prendendo spunto dal \emph{general model} di \cite{Kanellakis_Smolka-90}) sulla base della sintassi (linguaggio) e soprattutto della semantica (sistema di transizioni etichettato) definiti in precedenza; questi automi a stati finiti li chiamiamo comportamentali poich\'e rappresentano il comportamento dei servizi Web. Dopo aver dato una definizione formale di tale automa, riporteremo per ogni costrutto dei contratti il corrispondente AC.
\section{Definizione Automi Comportamentali}
Un automa comportamentale (AC) \`e una tupla
\[
  M = \automaton{M}
\]
in cui
\begin{itemize}
\item $Q_M$ \`e un insieme \emph{finito} di stati;

\item $\Sigma_M$ \`e un insieme finito di azioni tale che
  $\tau\not\in \Sigma_M$;

\item $\delta_M : Q_M \times \Sigma_M \cup \{\tau\} \to \wp(Q_M)$
  \`e la funzione di transizione;

\item $q_M \in Q_M$ \`e lo stato iniziale;

\item $F_M \subseteq Q_M$ \`e l'insieme degli stati finali.
\end{itemize}

Usiamo $a,b \in \Sigma_M$ per indicare azioni di input e $\co a,\co b$ per indicare le azioni di output corrispondenti. 
Usiamo $\alpha$ per indicare una generica azione dove l'azione interna \`e indicata con $\tau$.
%
Scriviamo $p \lred{\alpha}_M p'$ se e solo se $p' \in \delta_M(p,\alpha)$;
scriviamo $\wlred{\tau}_M$ per la chiusura riflessiva e
transitiva di $\lred{\tau}_M$; scriviamo $\wlred{\alpha}_M$ per
la relazione
$\wlred{\tau}_M\lred{\alpha}_M\wlred{\tau}_M$.  Sia
$\tauclosure_M(p) = \{ p' \mid p \wlred{\tau}_M p'\}$.

Dopo aver definito la struttura di un Automa Comportamentale con le varie diciture di supporto procediamo con la costruzione degli AC corrispondenti ad ogni costrutto della nostra grammatica, sulla base del sistema di transizioni etichettato. Per ogni attivit\`a utilizzeremo esempi, corrispondenti in BPEL, per comprendere meglio la costruzione.
\subsection{Fallimento: $\nullc$}
\begin{figure}[h]
  \centering
    \includegraphics{examples/success.A.eps}
  \caption{Automa Comportamentale dell'attivit\`a $\nullc$}
  \label{fig:win}
\end{figure}
Questo esempio rappresenta il cliente mai soddisfatto, quindi lo stato $q_0$ avr\`a come attivit\`a associata $\nullc$. Non ha esempi BPEL associati, in quanto \`e un'attivit\`a riservata ai soli clienti e ha solo un interesse teorico; ha la stessa rappresentazione del costrutto $\winc$, ma con semantica opposta. 
%Il cliente mai soddisfatto, denotato da $\nullc$, \`e definito come
%l'automa comportamentale
%\[
%\nullc \eqdef (\{\bot\}, \emptyset, \delta_\nullc, \bot, \emptyset)
%\]
%dove $\delta_\nullc(\bot,\mu) = \emptyset$.
\newpage
\subsection{Successo: $\winc$}
\begin{figure}[h]
  \centering
    \includegraphics{examples/success.A.eps}
  \caption{Automa Comportamentale dell'attivit\`a $\winc$}
  \label{fig:win}
\end{figure}
Questo esempio rappresenta l'attivit\`a BPEL: $empty$, denota il cliente soddisfatto e il servizio che non offre nulla; quindi lo stato $q_0$ avr\`a come attivit\`a associata $\winc$.
%Il cliente sempre soddisfatto e il servizio che non offre nulla,
%entrambi denotati da $\winc$, sono definiti come l'automa
%comportamentale
%\[
%\winc \eqdef (\{\top\}, \emptyset, \delta_\winc, \top, \{\top\})
%\]
%dove $\delta_\winc(\top,\mu) = \emptyset$.
\subsection{Azione: $\alpha$}
\begin{figure}[h]
  \centering
    \includegraphics{examples/action.A.eps}
  \caption{Automa Comportamentale dell'attivit\`a $\co a$ }
  \label{fig:alpha}
\end{figure}
Questo esempio rappresenta l'attivit\`a di output (stessa valenza anche per l'input): $ \co a$, effettuabile da un cliente o messa a disposizione da un servizio.\\ 
Attivit\`a associate agli stati:
\begin{itemize}
\item $q_0 = \overline a$
\item $q_1 = \winc$
\end{itemize}
%Il cliente soddisfatto dopo aver fatto l'azione $\alpha$ e il servizio
%che offre l'azione $\alpha$, entrambi denotati da $\alpha$, sono
%definiti come l'automa comportamentale
%\[
%\alpha \eqdef (\{\bot,\top\}, \{\alpha\}, \delta_\alpha, \bot, \{\top\})
%\]
%dove $\delta_\alpha$ \`e la pi\`u piccola funzione di transizione
%tale che $\delta_\alpha(\bot,\alpha) = \{\top\}$.
%
\newpage
\subsection{Scelta interna: $\oplus$}
\begin{figure}[h]
  \centering
    \includegraphics{examples/if.A.eps}
  \caption{Automa Comportamentale dell'attivit\`a $\overline a\oplus b$}
  \label{fig:oplus}
\end{figure}
Questo esempio rappresenta l'attivit\`a BPEL: $if \{ \co a\  b \}$, denota una scelta interna effettuabile localmente da chi espone tale attivit\`a, che porta in uno dei due stati dove da una parte l'azione da poter compiere \`e $\co a$ e dall'altra $b$.\\
Attivit\`a associate agli stati:
\begin{itemize}
\item $q_0 = \overline a\oplus b$
\item $q_1 = \overline a$
\item $q_2 = b$
\item $q_3 = \winc$
\end{itemize}
%
%Siano $M = \automaton{M}$ e $N = \automaton{N}$ due automi
%comportamentali tali che $Q_M \cap Q_N = \emptyset$ e $\bot \not\in
%Q_M\cup Q_N$. La \emph{scelta interna} di $M$ e $N$ \`e l'automa
%\[
%M\oplus N \eqdef (\{\bot\}\cup Q_M\cup Q_N, I_M \cup I_N, \delta_{M\oplus
%  N}, \bot, F_M \cup F_N)
%\]
%dove $\delta_{M\oplus N}$ \`e la pi\`u piccola funzione di transizione
%che include $\delta_M$ e $\delta_N$ e tale che $\delta_{M\oplus
%  N}(\bot,\varepsilon) = \{q_M,q_N\}$.
%
%\begin{proposition}
%Se $M$ e $N$ sono clienti (rispettivamente, servizi), allora $M\oplus
%N$ \`e un cliente (rispettivamente, un servizio).
%\end{proposition}
%\begin{proof}
%Siano $M$ e $N$ clienti, sia $p\in F_{M\oplus N}$ e supponiamo, senza
%perdere in generalit\`a, che $p\in F_M$.  Supponiamo inoltre $p
%\lred{\varepsilon}_{M\oplus N} p'$. Siccome $Q_M \cap Q_N =
%\emptyset$, abbiamo che $p \lred{\varepsilon}_M p'$ per costruzione di
%$\delta_{M\oplus N}$. Siccome $M$ \`e cliente, abbiamo $p'\in F_M$,
%dunque $p'\in F_M \cup F_N$.
%
%Siano $M$ e $N$ servizi, supponiamo $p \lred{\alpha}_{M\oplus N} p'$ e
%$p \lred{\varepsilon}_{M\oplus N} p''$. Deve essere $p \ne \bot$ e
%supponiamo, senza perdere in generalit\`a, che $p \in Q_M$. Per
%definizione di $\delta_{M\oplus N}$ abbiamo $p \lred{\alpha}_M p'$ e
%$p \lred{\varepsilon}_M p''$. Siccome $M$ \`e servizio, esiste $q\in
%Q_M$ tale che $p' \wlred{\varepsilon}_M q$ e $p'' \lred{\alpha}_M
%q$. Per definizione di $M\oplus N$, concludiamo $p'
%\wlred{\varepsilon}_{M\oplus N} q$ e $p'' \lred{\alpha}_{M\oplus N}
%q$.
%\end{proof}
\subsection{Scelta esterna: $+$}
\begin{figure}[h]
  \centering
    \includegraphics[height=3.6cm]{examples/pick.A.eps}
  \caption{Automa Comportamentale dell'attivit\`a $a+b$}
  \label{fig:plus}
\end{figure}
Questo esempio rappresenta l'attivit\`a BPEL: $pick \{ a\  b \}$, denota una scelta esterna effettuabile dalla parte remota, che interagisce con tale attivit\`a, la quale ha a disposizione o un'azione $a$ o un'azione $b$.\\
Attivit\`a associate agli stati:
\begin{itemize}
\item $q_0 = a+b$
\item $q_1 = \winc$
\end{itemize}
%Siano $M = \automaton{M}$ e $N = \automaton{N}$ due automi
%comportamentali tali che $Q_M \cap Q_N = \emptyset$ e $\bot \not\in
%Q_M\cup Q_N$. La \emph{scelta esterna} di $M$ e $N$ \`e l'automa
%\[
%M+N \eqdef (Q_M\cup\{\bot\}\times Q_N\cup\{\bot\}, I_M \cup I_N,
%\delta_{M+N}, (q_M,q_N), F_{M+N})
%\]
%dove $\delta_{M+N}$ \`e la pi\`u piccola funzione di transizione tale
%che
%\[
%\begin{array}{rcl}
%  \delta_{M+N}((p,q), \varepsilon)
%  & = &
%  \{(p', q) \mid p' \in \delta_M(p, \varepsilon)\}
%  \cup
%  \{(p, q') \mid q' \in \delta_N(q, \varepsilon)\}
%  \\
%  \delta_{M+N}((p,q), \alpha)
%  & = &
%  \{(p',\bot) \mid p' \in \delta_M(p, \alpha)\}
%  \cup
%  \{(\bot,q') \mid q' \in \delta_N(q, \alpha)\}
%  \\
%  \delta_{M+N}((p,\bot), \mu)
%  & = &
%  \{(p',\bot) \mid p' \in \delta_M(p,\mu)\}
%  \\
%  \delta_{M+N}((\bot,q), \mu)
%  & = &
%  \{(\bot,q') \mid q' \in \delta_N(q,\mu)\}
%\end{array}
%\]
%e
%\[
%F_{M+N} = \{(p,q) \mid p\in F_M \vee q\in F_N\}
%\cup
%\{(p,\bot) \mid p\in F_M\}
%\cup
%\{(\bot,q) \mid q\in F_N\}
%\]
%
%\begin{proposition}
%Se $M$ e $N$ sono clienti (rispettivamente, servizi), allora $M+
%N$ \`e un cliente (rispettivamente, un servizio).
%\end{proposition}
%
%\begin{proof}
%Siano $M$ e $N$ clienti, sia $(p,q)\in F_{M+N}$ e supponiamo, senza
%perdere in generalit\`a, che $p\in F_M$.  Supponiamo inoltre $(p,q)
%\lred{\varepsilon}_{M+N} (p',q)$. Siccome $Q_M \cap Q_N =
%\emptyset$, abbiamo che $p \lred{\varepsilon}_M p'$ per costruzione di
%$\delta_{M+N}$. Siccome $M$ \`e cliente, abbiamo $p'\in F_M$,
%dunque $(p',q)\in F_{M+N}$.
%
%Siano $M$ e $N$ servizi, supponiamo $(p,q) \lred{\alpha}_{M+N} (p',q)$ e
%$(p,q) \lred{\varepsilon}_{M+N} (p'',q)$. Supponiamo inoltre, senza perdere 
%in generalit\`a, che $p \in Q_M$. Per definizione di $\delta_{M+N}$ 
%abbiamo $p \lred{\alpha}_M p'$ e
%$p \lred{\varepsilon}_M p''$. Siccome $M$ \`e servizio, esiste $p'''\in
%Q_M$ tale che $p' \wlred{\varepsilon}_M p'''$ e $p'' \lred{\alpha}_M
%p'''$. Per definizione di $M+N$, concludiamo $(p',q)
%\wlred{\varepsilon}_{M+N} (p''',q)$ e $(p'',q) \lred{\alpha}_{M+N}
%(p''',q)$.
%\end{proof}
\subsection{Composizione sequenziale: ;}
\begin{center}
\begin{figure}[h]
  \centering
    \includegraphics{examples/sequence.A.eps}
  \caption{Automa Comportamentale dell'attivit\`a $a;\overline b$}
  \label{fig:sequence}
\end{figure}
\end{center}
Questo esempio rappresenta l'attivit\`a BPEL: $sequence \{ a\  \co b \}$, denota azioni effettuabili sequenzialmente da un servizio o un cliente, nel senso che per prima sar\`a disponibile un'azione $a$ e poi un'azione $\co b$.\\ 
Attivit\`a associate agli stati:
\begin{itemize}
\item $q_0 = a;\overline b$
\item $q_1 = \winc;\overline b$
\item $q_2 = \winc$
\end{itemize}
%Siano $M = \automaton{M}$ e $N = \automaton{N}$ due automi
%comportamentali tali che $Q_M \cap Q_N = \emptyset$ e $\bot \not\in
%Q_M\cup Q_N$. La \emph{composizione sequenziale} di $M$ e $N$ \`e
%l'automa
%\[
%M;N = (Q_M\cup\{\bot\}\times Q_N, I_M\cup I_N, \delta_{M;N}, (q_M,q_N), F_{M;N})
%\]
%dove
%\[
%\begin{array}{rcl}
%  \delta_{M;N}((p,q), \varepsilon)
%  & = &
%  \{(p', q) \mid p' \in \delta_M(p, \varepsilon)\}
%  \cup
%  \{(p, q') \mid q' \in \delta_N(q, \varepsilon)\}
%  \\
%  \delta_{M;N}((p,q), \alpha)
%  & = &
%  \{(p',q) \mid p' \in \delta_M(p, \alpha)\}
%  \cup
%  \{(\bot,q') \mid p\in F_M, q' \in \delta_N(q, \alpha)\}
%  \\
%  \delta_{M;N}((\bot,q), \mu)
%  & = &
%  \{(\bot,q') \mid q' \in \delta_N(q,\mu)\}
%\end{array}
%\]
%e
%\[
%F_{M;N} = \{(p,q) \mid p\in F_M \wedge q\in F_N\}
%\cup
%\{(\bot, q) \mid q\in F_N\}
%\]
%
%\begin{proposition}
%Se $M$ e $N$ sono clienti (rispettivamente, servizi), allora $M;
%N$ \`e un cliente (rispettivamente, un servizio).
%\end{proposition}
%
%\begin{proof}
%Siano $M$ e $N$ clienti, sia $(p,q)\in F_{M;N}$ e supponiamo che $p\in F_M$.  
%Supponiamo inoltre $(p,q)\lred{\varepsilon}_{M;N} (p,q')$. Per definizione
%di $\delta_{M;N}$ abbiamo $q\lred{\varepsilon}_N q'$ e siccome $N$ \`e cliente,
%abbiamo $q'\in F_N$, dunque $(p,q')\in F_M;N$.
%
%Siano $M$ e $N$ servizi, supponiamo $(p,q) \lred{\alpha}_{M;N} (p',q)$ e
%$(p,q) \lred{\varepsilon}_{M;N} (p'',q)$. Supponiamo inoltre, senza perdere 
%in generalit\`a, che $p \in Q_M$. Per definizione di $\delta_{M;N}$ 
%abbiamo $p \lred{\alpha}_M p'$ e
%$p \lred{\varepsilon}_M p''$. Siccome $M$ \`e servizio, esiste $p'''\in
%Q_M$ tale che $p' \wlred{\varepsilon}_M p'''$ e $p'' \lred{\alpha}_M
%p'''$. Per definizione di $M;N$, concludiamo $(p',q)
%\wlred{\varepsilon}_{M;N} (p''',q)$ e $(p'',q) \lred{\alpha}_{M;N}
%(p''',q)$.
%\end{proof}
\newpage
\subsection{Composizione parallela: $|$}
\begin{figure}[h]
  \centering
    \includegraphics[height=9cm]{examples/flow.A.eps}
  \caption{Automa Comportamentale dell'attivit\`a $a|\overline b|\overline c$}
  \label{fig:flow}  
\end{figure}
Questo esempio rappresenta l'attivit\`a BPEL: $flow \{ a\  \co b\  \co c \}$, denota l'esecuzione parallela delle azioni $a, \co b, \co c$; il parallelismo viene evidenziato dal fatto che qualunque sia l'azione che si intraprende si hanno poi disponibili, nel flusso di esecuzione, tutte le azioni rimanenti. Quindi indipendentemente dalle scelte che si effettuano, tutte le attivit\`a verranno eseguite.\\
Attivit\`a associate agli stati:
\begin{itemize}
\item $q_0 = a|\overline b|\overline c$
\item $q_1 = \winc|\overline b|\overline c$
\item $q_2 = a|\winc|\overline c$
\item $q_3 = a|\overline b|\winc$
\item $q_4 = \winc|\overline b|\winc$
\item $q_5 = a|\winc|\winc$
\item $q_6 = \winc$
\item $q_7 = \winc|\winc|\overline c$
\end{itemize}
\subsection{Ripetizione interna: $\circledast$}
\begin{figure}[h]
  \centering
    \includegraphics{examples/while.A.eps}
  \caption{Automa Comportamentale dell'attivit\`a $\overline a^\ast$}
  \label{fig:while}
\end{figure}
Questo esempio rappresenta l'attivit\`a BPEL: $while \{ \co a \}$, denota la ripetizione interna zero o piu volte, a discrezione della parte locale, dell'azione $\co a$.
\begin{itemize}
\item $q_0 = \overline a^\ast$
\item $q_1 = \winc$
\item $q_2 = \overline a;\overline a^\circledast$
\item $q_3 = \winc; \overline a^\circledast$
\end{itemize}
%Sia $M = \automaton{M}$ un automi comportamentali tale che $\bot
%\not\in Q_M$. La \emph{ripetizione interna} di $M$ \`e l'automa
%\[
%M^\circledast \eqdef (\{\bot,\top\}\cup (Q_M\times Q_M\cup\{\bot\}),
%I_M, \delta_{M^\circledast}, \bot, F_{M^\circledast})
%\]
%dove
%\[
%\begin{array}{rcl}
%  \delta_{M^\circledast}(\bot, \varepsilon)
%  & = &
%  \{\top, (q_M,\bot), (q_M,q_M)\}
%  \\
%  \delta_{M^\circledast}((p,q), \varepsilon)
%  & = &
%  \{(p',q) \mid p' \in \delta_M(p, \alpha)\}
%  \cup
%  \{(p,q') \mid q' \in \delta_N(q, \alpha)\}
%  \\
%  \delta_{M^\circledast}((p,q), \alpha)
%  & = &
%  \{(p',q) \mid p' \in \delta_M(p, \alpha)\}
%  \cup
%  \{(q',\bot) \mid p\in F_M, q'\in\delta_M(q,\alpha)\}
%  \\
%  & & \qquad {} \cup
%  \{(q',q_M) \mid p\in F_M, q'\in\delta_M(q,\alpha)\}
%  \\
%  \delta_{M^\circledast}((p,\bot), \mu)
%  & = &
%  \{(p',\bot) \mid p' \in \delta_M(p,\mu)\}
%\end{array}
%\]
%e
%\[
%F_{M^\circledast} = \{\top\} \cup \{(p,\bot) \mid p\in F_M\}
%\cup \{(p,q) \mid p,q\in F_M\}
%\]
%
%\begin{proposition}
%Se $M$ e $N$ sono clienti (rispettivamente, servizi), allora $M\circledast
%N$ \`e un cliente (rispettivamente, un servizio).
%\end{proposition}
%
%\begin{proof}
%Sia $M$ un cliente , sia $(p,q)\in F_{M^\circledast}$ e supponiamo che $q = \bot.$  
%Supponiamo inoltre $(p,q)\lred{\varepsilon}_{M^\circledast} (p',q)$. Per definizione
%di $\delta_{M^\circledast}$ abbiamo $p\lred{\varepsilon}_M p'$ e siccome $M$ \`e cliente,
%abbiamo $p'\in F_M$, dunque $(p,q')\in F_{M^\circledast}$.
%
%Sia $M$ un servizio, supponiamo $(p,q) \lred{\alpha}_{M^\circledast} (p',q)$ e
%$(p,q) \lred{\varepsilon}_{M^\circledast} (p'',q)$. Supponiamo inoltre, senza perdere 
%in generalit\`a, che $p \in Q_M$. Per definizione di $\delta_{M^\circledast}$ 
%abbiamo $p \lred{\alpha}_M p'$ e
%$p \lred{\varepsilon}_M p''$. Siccome $M$ \`e servizio, esiste $p'''\in
%Q_M$ tale che $p' \wlred{\varepsilon}_M p'''$ e $p'' \lred{\alpha}_M
%p'''$. Per definizione di $M^\circledast$, concludiamo $(p',q)
%\wlred{\varepsilon}_{M^\circledast} (p''',q)$ e $(p'',q) \lred{\alpha}_{M^\circledast}
%(p''',q)$.
%\end{proof}
\newpage
\subsection{Ripetizione esterna: $\ast$}
\begin{figure}[h]
  \centering
    \includegraphics{examples/repeat.A.eps}
  \caption{Automa Comportamentale dell'attivit\`a $\overline a^\ast$}
  \label{fig:repeat}
\end{figure}
Questo esempio rappresenta l'attivit\`a: $repeat \{ \co a \}$, denota la ripetizione una o piu volte, a discrezione della parte remota, dell'azione $\co a$. Quest'attivit\`a non \`e presente nelle specifiche bpel ma l'abbiamo introdotta per dare la possibilit\`a al cliente di "`"`chiamare in causa"'"' il servizio una o pi\`u volte, in quanto il corpo di questo costrutto racchiuder\`a proprio il servizio.\\
\begin{itemize}
\item $q_0 = \overline a^\ast$
\item $q_1 = \winc;\overline a^\ast$
\end{itemize}
%Sia $M = \automaton{M}$ un automi comportamentali tale che $\bot
%\not\in Q_M$. La \emph{ripetizione esterna} di $M$ \`e l'automa
%\[
%M^\ast \eqdef (Q_M\times Q_M, I_M, \delta_{M^\ast}, (q_M,q_M), F_{M^\ast})
%\]
%dove
%\[
%\begin{array}{rcl}
%  \delta_{M^\ast}((p,q), \varepsilon)
%  & = &
%  \{(p', q) \mid p' \in \delta_M(p, \varepsilon)\}
%  \cup
%  \{(p, q') \mid q' \in \delta_M(q, \varepsilon)\}
%  \\
%  \delta_{M^\ast}((p,q), \alpha)
%  & = &
%  \{(p',q) \mid p'\in\delta_M(p,\alpha)\}
%  \cup
%  \{(q',q_M) \mid p\in F_M \wedge q'\in\delta_M(q,\alpha)\}
%\end{array}
%\]
%e
%\[
%F_{M^\ast} = \{(p,q) \mid p,q\in \eclosure(q_M)\cup F_M\}
%\]
%
%\begin{proposition}
%Se $M$ e $N$ sono clienti (rispettivamente, servizi), allora $M\ast
%N$ \`e un cliente (rispettivamente, un servizio).
%\end{proposition}
%
%\begin{proof}
%Sia $M$ un cliente, sia $(p,q)\in F_{M^\ast}$ e supponiamo che $p\in F_M$.  
%Supponiamo inoltre $(p,q)\lred{\varepsilon}_{M^\ast} (p,q')$. Per definizione
%di $\delta_{M^\ast}$ abbiamo $q\lred{\varepsilon}_M q'$ e siccome $M$ \`e cliente,
%abbiamo $q'\in F_N$, dunque $(p,q')\in F_{M^\ast}$.
%
%Sia $M$ un servizio , supponiamo $(p,q) \lred{\alpha}_{M^\ast} (p',q)$ e
%$(p,q) \lred{\varepsilon}_{M^\ast} (p'',q)$. Supponiamo inoltre, senza perdere 
%in generalit\`a, che $p \in Q_M$. Per definizione di $\delta_{M^\ast}$ 
%abbiamo $p \lred{\alpha}_M p'$ e
%$p \lred{\varepsilon}_M p''$. Siccome $M$ \`e servizio, esiste $p'''\in
%Q_M$ tale che $p' \wlred{\varepsilon}_M p'''$ e $p'' \lred{\alpha}_M
%p'''$. Per definizione di $M^\ast$, concludiamo $(p',q)
%\wlred{\varepsilon}_{M^\ast} (p''',q)$ e $(p'',q) \lred{\alpha}_{M^\ast}
%(p''',q)$.
%\end{proof}
Dopo aver formalizzato e rappresentato graficamente gli Automi Comportamentali associati ai contratti, mettiamo in relazione i clienti con i servizi definendo quano un "`"`cliente \`e soddisfatto"'"' nei confronti di un servizio e quando un servizio \`e "`"`sottoservizio"'"' di un altro. 
\section{Interazione cliente-servizio}
Prima di affrontare le definizioni legate all'interazione cliente-servizio diamo delle notazioni ausiliarie che utilizzeremo in questa sezione e nei capitoli successivi.
\label{sec:int_c-s}
\begin{notation}
\label{not:int_c-s}
\[
\begin{array}{rcl}
  \stable(P) & = & \{ p' \mid \exists p \in P : p \wlred{\tau} p' \nlred{\tau} \} \\
  S(p) & = & \{ \alpha \mid p \lred{\alpha} \} \\
  P(\alpha) & = & \{ p' \mid \exists p\in P : p \wlred{\tau}\lred{\alpha} p' \} \\
  P(s) & = &
  \begin{cases}
    P & \text{se $s = \tau$} \\
    P(\alpha)(s') & \text{se $s = \alpha s'$}
  \end{cases}
\end{array}
\]
\end{notation}

\begin{definition}[Cliente soddisfatto]
\label{def:cliente_sodd}
Siano $p$ e $q$ stati di un cliente e un servizio, rispettivamente.
Una \emph{interazione} di $p$ e $q$ \`e una sequenza $p_0 \parop q_0
\lred{} p_1 \parop q_1 \lred{} \cdots$ tale che $p_0 = p$, $q_0 = q$ e
inoltre per ogni coppia di stati $p_{i+1} \parop q_{i+1}$ successiva a
quella iniziale abbiamo che:
\begin{itemize}
\item $p_i \lred{\tau} p_{i+1}$ e $q_{i+1} = q_i$, oppure

\item $p_{i+1} = p_i$ e $q_i \lred{\tau} q_{i+1}$, oppure

\item esiste $\alpha$ tale che $p_i \lred{\alpha} p_{i+1}$ e $q_i \lred{\co \alpha}
  q_{i+1}$.
\end{itemize}

Indichiamo con $\wlred{}$ la chiusura riflessiva e transitiva della
relazione $\lred{}$ tra le coppie di stati. Diciamo che $p$ \`e
soddisfatto da $q$, notazione $p \scomp q$, se ogni interazione
massimale finita $p_0 \parop q_0 \wlred{} p_n \parop q_n$ di $p$ e $q$
\`e tale che $p_n$ \`e finale.
\end{definition}

\begin{definition}[Semantica di un servizio]
\label{def:subc}
La semantica di un servizio $p$, denotata da $\bsem{p}$, \`e l'insieme
dei clienti soddisfatti da $p$, ovvero $\bsem{p} \eqdef \{ r \mid r
\scomp p \}$.
\end{definition}

\begin{definition}[Sottoservizio]
Diciamo che $p$ \`e un \emph{sottoservizio} di $q$, notazione $p \subc
q$, se tutti i clienti soddisfatti da $p$ sono soddisfatti anche da
$q$, ovvero se $\bsem{p} \subseteq \bsem{q}$.  Indichiamo con $\eqc$
l'equivalenza indotta da $\subc$, ovvero $p \eqc q$ se $\bsem{p} =
\bsem{q}$.
\end{definition}

\begin{notation} 
Nel seguito sar\`a comodo estendere il concetto di soddisfazione di un
cliente nei confronti di \emph{un insieme di stati} di un servizio. In
particolare, diciamo che $p$ \`e soddisfatto da $Q$, notazione $p
\scomp Q$, se per ogni $q \in Q$ abbiamo che $p \scomp q$.  Estendiamo
quindi il concetto di semantica di un servizio a insiemi di stati in
modo che $\bsem{P} \eqdef \{ r \mid r \scomp P \}$.  A questo punto
possiamo estendere il concetto di sottoservizio a insiemi di stati in
modo che $P \subc Q$ se $\bsem{P} \subseteq \bsem{Q}$ e che $P \eqc Q$
se $\bsem{P} = \bsem{Q}$.
\end{notation}

\begin{definition}[Sottoservizio coinduttivo]
\label{def:subccoind}
La relazione $\rel{R}$ \`e un \emph{sottoservizio coinduttivo} se $P
\rel{R} Q$ implica:
\begin{enumerate}
\item per ogni $q\in\stable(Q)$ esiste $p\in\stable(P)$ tale che
  $S(p)\subseteq S(q)$;  
\item se esiste $q\in Q$ tale che $q \wlred{\alpha}$ allora esiste $p\in P$
  tale che $p \wlred{\alpha}$ e $P(\alpha) \rel{R} Q(\alpha)$. 
\end{enumerate}
\end{definition}

\begin{theorem}
Per ogni $P$ e $Q$ abbiamo $P \subc Q$ se e solo se esiste un
sottoservizio coinduttivo $\rel{R}$ tale che $P \rel{R} Q$.
\end{theorem}
\begin{proof}
(Parte ``solo se'') \`E sufficiente dimostrare che $\subc$ \`e un
  sottoservizio coinduttivo.  Sia $P \subc Q$.
%
  Per quanto riguarda la condizione~(1) nella
  Definizione~\ref{def:subccoind}, sia $\stable(P) =
  \{p_1,\dots,p_n\}$ e supponiamo per assurdo che esista $q\in
  \stable(Q)$ tale che per ogni $1\le i\le n$ abbiamo $S(p_i)
  \not\subseteq S(q)$. In altri termini, per ogni $1\le i\le n$ esiste
  $\alpha_i \in S(p_i) \setminus S(q)$. Sia $C$ il cliente
  \[
  C \eqdef (\{p_0, p_1\}, \{{\alpha_1},\dots,{\alpha_n}\},
  \delta, p_0, \{p_1\})
  \]
  dove $\delta$ \`e la pi\`u piccola funzione di transizione tale che
  $\delta(p_0, {\alpha_i}) = \{p_1\}$ per ogni $1\le i\le n$.  Chiaramente
  $p_0 \scomp P$ mentre $p_0 \not\scomp Q$ a causa dell'interazione
  \[
    p_0 \parop q_0 \wlred{} p_0 \parop q \nlred{}
  \]
  dal momento che $S(p_0) \cap S(q) = \emptyset$ e che $p_0$ non \`e
  finale, ma questo contraddice $P \subc Q$.
%
  Per quanto riguarda la condizione~(2) nella
  Definizione~\ref{def:subccoind}, supponiamo per assurdo che esistano
  $q\in Q$ e $\alpha$ tali che $q \wlred{\alpha}$ ma per ogni $p \in P$ abbiamo
  $p \nwlred{\alpha}$ e sia $q'$ tale che $q \wlred{\alpha} q' \nlred{}$. Sia
  $C$ il cliente
  \[
  C \eqdef (\{p_0, p_1\}, \{\alpha\}, \delta, p_0, \{p_0\})
  \]
  dove $\delta$ \`e la pi\`u piccola funzione di transizione tale che
  $\delta(p_0, \alpha) = \{p_1\}$. Chiaramente $p_0 \scomp P$ mentre $p_0
  \not\scomp Q$ a causa dell'interazione $p_0 \parop q \wlred{} p_1
  \parop q' \nlred{}$ dal momento che $p_1$ non ha transizioni e non
  \`e finale. Per concludere la dimostrazione, sia $C=\automaton{C}$
  un cliente tale che $p\not\in Q_C$ e $p_C \scomp P(\alpha)$. Vogliamo
  dimostrare che $p_C \scomp Q(\alpha)$. Sia $D$ il cliente
  \[
  D \eqdef (\{p\}\cup Q_C, \Sigma_C\cup\{\alpha\}, \delta_D, p, \{p\}\cup F_C)
  \]
  dove $\delta_D$ \`e la pi\`u piccola funzione di transizione che
  include $\delta_C$ e tale che $\delta_D(p, \alpha) = \{p_C\}$.
  Osserviamo che $p \scomp P$, da cui deduciamo $p \scomp Q$ in quanto
  $P \subc Q$, ma questo implica $p_C \scomp Q(\alpha)$. Siccome $C$ \`e
  stato scelto arbitrariamente possiamo concludere $P(\alpha) \subc Q(\alpha)$.

(Parte ``se'') Dobbiamo mostrare che $\subc$ \`e il pi\`u grande
  sottocontratto coinduttivo. Sia $\rel{R}$ un sottocontratto
  coinduttivo e supponiamo $P \rel{R} Q$. Supponiamo inoltre che
  $C=\automaton{C}$ sia un cliente tale che $p_C \scomp P$ e sia
  \[
  p_0 \parop q_0 \lred{} \cdots \lred{} p_n \parop q_n \nlred{}
  \]
  una interazione massimale finita di $p_C$ e $q \in Q$. In
  particolare, sia $s$ la sequenza (finita) di azioni tali che $p_0
  \wlred{s} p_n$ e $q_0 \wlred{s} q_n$. Da $P \rel{R} Q$ e dalla
  condizione~(2) nella Definizione~\ref{def:subccoind} deduciamo che
  $P(s) \rel{R} Q(s)$. Dalla condizione~(1) otteniamo inoltre che
  esistono $p \in P$ e $p'\in\stable(P(s))$ tali che $p \wlred{s} p'$
  e $S(p') \subseteq S(q_n)$. Dunque $p_0 \parop p \wlred{} p_n \parop
  p' \nlred{}$ \`e una interazione massimale finita di $p_C$ e $p\in
  P$.  Dall'ipotesi $p_C \scomp P$ osserviamo che $p_n$ deve essere
  finale, dunque $p_C \scomp Q$.
\end{proof}

\begin{example}
Nella \figurename~\ref{fig:set_state} sono rappresentati due servizi, rispettivamente $\co a;b +\co a;c$ in \figurename~\ref{fig:set_state.A} e $\co a;(b \oplus c)$ in \figurename~\ref{fig:set_state1.A}, in cui uno \`e sottoservizio dell'altro: $\co a;b +\co a;c \subc \co a;(b \oplus c)$. Analizzando i due automi notiamo che in entrambi i casi la prima azione disponibile \`e $\overline a$, dopo la quale: nel primo esempio possiamo disporre dell'azione $b$ o dell'azione $c$, invece nel secondo avremo a disposizione l'attivit\`a $(b \oplus c)$. Da tale considerazione possiamo evincere che in entrambi i casi effettuando un'azione $\co a$ giungiamo in una situazione in cui $b \not\subc (b \oplus c)$ o $c \not\subc (b \oplus c)$ ed \`e qui che scaturisce l'esigenza di ragionare in termini di \emph{insieme di stati}, poich\'e se noi consideriamo i successori di $\co a$ singolarmente, come abbiamo fatto, saremmo tentati di concludere che $\co a;b +\co a;c \not\subc \co a;(b \oplus c)$. Quindi lo stato che soddisfer\`a il cliente, in questa circostanza, sar\`a l'insieme degli stati $\{b,c\}$. Per concludere estendendo il concetto di sottoservizio a insieme di stati, dopo l'azione $\co a$ avremo che: $\{b,c\} \subc (b \oplus c)$ e quindi ogni cliente $p$, tale che $p \scomp \{b,c\}$, deve essere: $p \scomp b$ e $p \scomp c$.
\end{example}

\begin{figure}[h]
\centering
\subfigure[$\co a;b +\co a;c$ \label{fig:set_state.A}]%
{\includegraphics{examples/set_state.A.eps}}
\hspace{3cm}
\subfigure[$\co a;(b \oplus c)$ \label{fig:set_state1.A}]%
{\includegraphics{examples/set_state1.A.eps}}
\caption{AC delle attivit\`a $\co a;b +\co a;c$ e $\co a;(b \oplus c)$}
\label{fig:set_state}
\end{figure}